1 /-
2 Copyright (c) 2019 Scott Morrison. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Scott Morrison
5 -/
6 import algebra.category.CommRing.basic
src └─────────────────────────────┘
7 import category_theory.limits.limits
src └───────────────────────────┘
8
9 /-!
10 # The category of commutative rings has all colimits.
11
12 This file uses a "pre-automated" approach, just as for `Mon/colimits.lean`.
13 It is a very uniform approach, that conceivably could be synthesised directly
14 by a tactic that analyses the shape of `comm_ring` and `ring_hom`.
15 -/
16
17 universes u v
18
19 open category_theory
20 open category_theory.limits
21
22 -- [ROBOT VOICE]:
23 -- You should pretend for now that this file was automatically generated.
24 -- It follows the same template as colimits in Mon.
25 -- Note that this means this file does not meet documentation standards.
26 /-
27 `#print comm_ring` says:
28
29 structure comm_ring : Type u → Type u
30 fields:
31 comm_ring.zero : Π (α : Type u) [c : comm_ring α], α
32 comm_ring.one : Π (α : Type u) [c : comm_ring α], α
33 comm_ring.neg : Π {α : Type u} [c : comm_ring α], α → α
34 comm_ring.add : Π {α : Type u} [c : comm_ring α], α → α → α
35 comm_ring.mul : Π {α : Type u} [c : comm_ring α], α → α → α
36
37 comm_ring.zero_add : ∀ {α : Type u} [c : comm_ring α] (a : α), 0 + a = a
38 comm_ring.add_zero : ∀ {α : Type u} [c : comm_ring α] (a : α), a + 0 = a
39 comm_ring.one_mul : ∀ {α : Type u} [c : comm_ring α] (a : α), 1 * a = a
40 comm_ring.mul_one : ∀ {α : Type u} [c : comm_ring α] (a : α), a * 1 = a
41 comm_ring.add_left_neg : ∀ {α : Type u} [c : comm_ring α] (a : α), -a + a = 0
42 comm_ring.add_comm : ∀ {α : Type u} [c : comm_ring α] (a b : α), a + b = b + a
43 comm_ring.mul_comm : ∀ {α : Type u} [c : comm_ring α] (a b : α), a * b = b * a
44 comm_ring.add_assoc : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), a + b + c_1 = a + (b + c_1)
45 comm_ring.mul_assoc : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), a * b * c_1 = a * (b * c_1)
46 comm_ring.left_distrib : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
st ┴
47 comm_ring.right_distrib : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
48 -/
49
50 namespace CommRing.colimits
51
52 variables {J : Type v} [small_category J] (F : J ⥤ CommRing.{v})
id └────────────┘ ┴ └──────┘
src └────────────┘ ┴ └──────┘
typ └────────────┘ ┴ └──────┘
doc └────────────┘ ┴ └──────┘
53
54 inductive prequotient
55 -- There's always `of`
56 | of : Π (j : J) (x : F.obj j), prequotient
id └──┘ ┴
src └──┘
typ └──┘ ┴
57 -- Then one generator for each operation
58 | zero {} : prequotient
59 | one {} : prequotient
60 | neg : prequotient → prequotient
61 | add : prequotient → prequotient → prequotient
62 | mul : prequotient → prequotient → prequotient
63
64 open prequotient
65
66 inductive relation : prequotient F → prequotient F → Prop
id └─────────┘ └─────────┘
src └─────────┘ └─────────┘
typ └─────────┘ └─────────┘
67 -- Make it an equivalence relation:
68 | refl : Π (x), relation x x
id ┴ ┴ ┴
typ ┴ ┴ ┴
69 | symm : Π (x y) (h : relation x y), relation y x
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
70 | trans : Π (x y z) (h : relation x y) (k : relation y z), relation x z
id ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
71 -- There's always a `map` relation
72 | map : Π (j j' : J) (f : j ⟶ j') (x : F.obj j), relation (of j' (F.map f x)) (of j x)
id ┴ ┴ └┘ └──┘ ┴ └┘ └┘ └──┘ ┴ ┴ └┘ ┴ ┴
src ┴ └──┘ └┘ └──┘ └┘
typ ┴ ┴ └┘ └──┘ ┴ └┘ └┘ └──┘ ┴ ┴ └┘ ┴ ┴
73 -- Then one relation per operation, describing the interaction with `of`
74 | zero : Π (j), relation (of j 0) zero
id ┴ └┘ ┴ └──┘
src └┘ └──┘
typ ┴ └┘ ┴ └──┘
75 | one : Π (j), relation (of j 1) one
id ┴ └┘ ┴ └─┘
src └┘ └─┘
typ ┴ └┘ ┴ └─┘
76 | neg : Π (j) (x : F.obj j), relation (of j (-x)) (neg (of j x))
id ┴ └──┘ ┴ └┘ ┴ ┴┴ └─┘ └┘ ┴ ┴
src └──┘ └┘ ┴ └─┘ └┘
typ ┴ └──┘ ┴ └┘ ┴ ┴┴ └─┘ └┘ ┴ ┴
77 | add : Π (j) (x y : F.obj j), relation (of j (x + y)) (add (of j x) (of j y))
id ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘ └┘ ┴ └─┘ └┘ └┘
typ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴
78 | mul : Π (j) (x y : F.obj j), relation (of j (x * y)) (mul (of j x) (of j y))
id ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘ └┘ ┴ └─┘ └┘ └┘
typ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴
79 -- Then one relation per argument of each operation
80 | neg_1 : Π (x x') (r : relation x x'), relation (neg x) (neg x')
id ┴ └┘ └──────┘ ┴ └┘ └─┘ ┴ └─┘ └┘
src └─┘ └─┘
typ ┴ └┘ └──────┘ ┴ └┘ └─┘ ┴ └─┘ └┘
81 | add_1 : Π (x x' y) (r : relation x x'), relation (add x y) (add x' y)
id ┴ └┘ ┴ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ └┘ ┴
src └─┘ └─┘
typ ┴ └┘ ┴ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ └┘ ┴
82 | add_2 : Π (x y y') (r : relation y y'), relation (add x y) (add x y')
id ┴ ┴ └┘ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘
src └─┘ └─┘
typ ┴ ┴ └┘ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘
83 | mul_1 : Π (x x' y) (r : relation x x'), relation (mul x y) (mul x' y)
id ┴ └┘ ┴ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ └┘ ┴
src └─┘ └─┘
typ ┴ └┘ ┴ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ └┘ ┴
84 | mul_2 : Π (x y y') (r : relation y y'), relation (mul x y) (mul x y')
id ┴ ┴ └┘ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘
src └─┘ └─┘
typ ┴ ┴ └┘ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘
85 -- And one relation per axiom
86 | zero_add : Π (x), relation (add zero x) x
id ┴ └─┘ └──┘ ┴ ┴
src └─┘ └──┘
typ ┴ └─┘ └──┘ ┴ ┴
87 | add_zero : Π (x), relation (add x zero) x
id ┴ └─┘ ┴ └──┘ ┴
src └─┘ └──┘
typ ┴ └─┘ ┴ └──┘ ┴
88 | one_mul : Π (x), relation (mul one x) x
id ┴ └─┘ └─┘ ┴ ┴
src └─┘ └─┘
typ ┴ └─┘ └─┘ ┴ ┴
89 | mul_one : Π (x), relation (mul x one) x
id ┴ └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ ┴ └─┘ ┴ └─┘ ┴
90 | add_left_neg : Π (x), relation (add (neg x) x) zero
id ┴ └─┘ └─┘ ┴ ┴ └──┘
src └─┘ └─┘ └──┘
typ ┴ └─┘ └─┘ ┴ ┴ └──┘
91 | add_comm : Π (x y), relation (add x y) (add y x)
id ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └─┘
typ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
92 | mul_comm : Π (x y), relation (mul x y) (mul y x)
id ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └─┘
typ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
93 | add_assoc : Π (x y z), relation (add (add x y) z) (add x (add y z))
id ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
src └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
94 | mul_assoc : Π (x y z), relation (mul (mul x y) z) (mul x (mul y z))
id ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
src └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
95 | left_distrib : Π (x y z), relation (mul x (add y z)) (add (mul x y) (mul x z))
id ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴
96 | right_distrib : Π (x y z), relation (mul (add x y) z) (add (mul x z) (mul y z))
id ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴
97
98 def colimit_setoid : setoid (prequotient F) :=
id └────┘ └─────────┘ ┴
src └────┘ └─────────┘
typ └────┘ └─────────┘ ┴
99 { r := relation F, iseqv := ⟨relation.refl, relation.symm, relation.trans⟩ }
id └──────┘ ┴ └───────────┘ └───────────┘ └────────────┘
src └──────┘ └───────────┘ └───────────┘ └────────────┘
typ └──────┘ ┴ └───────────┘ └───────────┘ └────────────┘
100 attribute [instance] colimit_setoid
id └────────────┘
src └────────────┘
typ └────────────┘
101
102 def colimit_type : Type v := quotient (colimit_setoid F)
id └──────┘ └────────────┘ ┴
src └──────┘ └────────────┘
typ └──────┘ └────────────┘ ┴
103
104 instance : comm_ring (colimit_type F) :=
id └───────┘ └──────────┘ ┴
src └───────┘ └──────────┘
typ └───────┘ └──────────┘ ┴
105 { zero :=
106 begin
st └─────
107 exact quot.mk _ zero
id └─────┘ └──┘
src └────┘ └─┘└──┘└
typ └────┘└─────┘└─┘└──┘└
doc └────┘ └─┘ └
txt └────┘ └─┘ └
par └────┘ └─┘ └
pid ┴ └─┘ └
st ─────────────────────────
108 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
109 one :=
110 begin
st └─────
111 exact quot.mk _ one
id └─────┘ └─┘
src └────┘ └─┘└─┘└
typ └────┘└─────┘└─┘└─┘└
doc └────┘ └─┘ └
txt └────┘ └─┘ └
par └────┘ └─┘ └
pid ┴ └─┘ └
st ────────────────────────
112 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
113 neg :=
114 begin
st └─────
115 fapply @quot.lift,
id └───────┘
src └─────┘
typ └─────┘ └───────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
st ────────────────────┘└─
116 { intro x,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ─────┘└─────┘└─
117 exact quot.mk _ (neg x) },
id └─────┘ └─┘ ┴
src └────┘ └─┘ └─┘┴ └┘
typ └────┘└─────┘└─┘ └─┘┴┴└┘
doc └────┘ └─┘ ┴ └┘
txt └────┘ └─┘ ┴ └┘
par └────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ─────────────────────────────┘└┘└
118 { intros x x' r,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ──────────────────┘└─
119 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
120 exact relation.neg_1 _ _ r },
id └────────────┘ ┴
src └────┘└────────────┘└───┘ ┴
typ └────┘└────────────┘└───┘┴┴
doc └────┘ └───┘ ┴
txt └────┘ └───┘ ┴
par └────┘ └───┘ ┴
pid ┴ └───┘ ┴
st ────────────────────────────────┘└──
121 end,
st ────┘
122 add :=
123 begin
st └─────
124 fapply @quot.lift _ _ ((colimit_type F) → (colimit_type F)),
id └───────┘ └──────────┘ └──────────┘ ┴
src └─────┘ └───┘ ┴ └┘ ┴ └──────────┘┴ └┘
typ └─────┘ └───────┘└───┘ └──────────┘┴ └┘ ┴ └──────────┘┴┴└┘
doc └─────┘ └───┘ ┴ └┘ ┴ ┴ └┘
txt └─────┘ └───┘ ┴ └┘ ┴ ┴ └┘
par └─────┘ └───┘ ┴ └┘ ┴ ┴ └┘
pid ┴ └───┘ ┴ └┘ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────┘└─
125 { intro x,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ─────┘└─────┘└─
126 fapply @quot.lift,
id └───────┘
src └─────┘
typ └─────┘ └───────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
st ──────────────────────┘└─
127 { intro y,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ───────┘└─────┘└─
128 exact quot.mk _ (add x y) },
id └─────┘ └─┘ ┴ ┴
src └────┘ └─┘ └─┘┴ ┴ └┘
typ └────┘└─────┘└─┘ └─┘┴┴┴┴└┘
doc └────┘ └─┘ ┴ ┴ └┘
txt └────┘ └─┘ ┴ ┴ └┘
par └────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴
st ─────────────────────────────────┘└┘└
129 { intros y y' r,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ────────────────────┘└─
130 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────┘└─
131 exact relation.add_2 _ _ _ r } },
id └────────────┘ ┴
src └────┘└────────────┘└─────┘ ┴
typ └────┘└────────────┘└─────┘┴┴
doc └────┘ └─────┘ ┴
txt └────┘ └─────┘ ┴
par └────┘ └─────┘ ┴
pid ┴ └─────┘ ┴
st ────────────────────────────────────┘└──┘└
132 { intros x x' r,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ──────────────────┘└─
133 funext y,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ─────────────┘└─
134 induction y,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ────────────────┘└─
135 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
136 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
137 { exact relation.add_1 _ _ _ r },
id └────────────┘ ┴
src └────┘└────────────┘└─────┘ ┴
typ └────┘└────────────┘└─────┘┴┴
doc └────┘ └─────┘ ┴
txt └────┘ └─────┘ ┴
par └────┘ └─────┘ ┴
pid ┴ └─────┘ ┴
st ───────┘└───────────────────────────┘└┘└
138 { refl } },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────────┘└────
139 end,
st ────┘
140 mul :=
141 begin
st └─────
142 fapply @quot.lift _ _ ((colimit_type F) → (colimit_type F)),
id └───────┘ └──────────┘ ┴
src └─────┘ └───┘ ┴ └┘ ┴ └──────────┘┴ └┘
typ └─────┘ └───────┘└───┘ ┴ └┘ ┴ └──────────┘┴┴└┘
doc └─────┘ └───┘ ┴ └┘ ┴ ┴ └┘
txt └─────┘ └───┘ ┴ └┘ ┴ ┴ └┘
par └─────┘ └───┘ ┴ └┘ ┴ ┴ └┘
pid ┴ └───┘ ┴ └┘ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────┘└─
143 { intro x,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ─────┘└─────┘└─
144 fapply @quot.lift,
id └───────┘
src └─────┘
typ └─────┘ └───────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
st ──────────────────────┘└─
145 { intro y,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ───────┘└─────┘└─
146 exact quot.mk _ (mul x y) },
id └─────┘ └─┘ ┴ ┴
src └────┘ └─┘ └─┘┴ ┴ └┘
typ └────┘└─────┘└─┘ └─┘┴┴┴┴└┘
doc └────┘ └─┘ ┴ ┴ └┘
txt └────┘ └─┘ ┴ ┴ └┘
par └────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴
st ─────────────────────────────────┘└┘└
147 { intros y y' r,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ────────────────────┘└─
148 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────┘└─
149 exact relation.mul_2 _ _ _ r } },
id └────────────┘ ┴
src └────┘└────────────┘└─────┘ ┴
typ └────┘└────────────┘└─────┘┴┴
doc └────┘ └─────┘ ┴
txt └────┘ └─────┘ ┴
par └────┘ └─────┘ ┴
pid ┴ └─────┘ ┴
st ────────────────────────────────────┘└──┘└
150 { intros x x' r,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ──────────────────┘└─
151 funext y,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ─────────────┘└─
152 induction y,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ────────────────┘└─
153 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
154 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
155 { exact relation.mul_1 _ _ _ r },
id └────────────┘ ┴
src └────┘└────────────┘└─────┘ ┴
typ └────┘└────────────┘└─────┘┴┴
doc └────┘ └─────┘ ┴
txt └────┘ └─────┘ ┴
par └────┘ └─────┘ ┴
pid ┴ └─────┘ ┴
st ───────┘└───────────────────────────┘└┘└
156 { refl } },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────────┘└────
157 end,
st ────┘
158 zero_add := λ x,
id ┴
typ ┴
159 begin
st └─────
160 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
161 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
162 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
163 apply relation.zero_add,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────┘└─
164 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
165 end,
st ────┘
166 add_zero := λ x,
id ┴
typ ┴
167 begin
st └─────
168 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
169 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
170 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
171 apply relation.add_zero,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────┘└─
172 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
173 end,
st ────┘
174 one_mul := λ x,
id ┴
typ ┴
175 begin
st └─────
176 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
177 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
178 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
179 apply relation.one_mul,
id └──────────────┘
src └────┘└──────────────┘
typ └────┘└──────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────┘└─
180 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
181 end,
st ────┘
182 mul_one := λ x,
id ┴
typ ┴
183 begin
st └─────
184 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
185 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
186 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
187 apply relation.mul_one,
id └──────────────┘
src └────┘└──────────────┘
typ └────┘└──────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────┘└─
188 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
189 end,
st ────┘
190 add_left_neg := λ x,
id ┴
typ ┴
191 begin
st └─────
192 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
193 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
194 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
195 apply relation.add_left_neg,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
196 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
197 end,
st ────┘
198 add_comm := λ x y,
id ┴ ┴
typ ┴ ┴
199 begin
st └─────
200 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
201 induction y,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
202 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
203 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
204 apply relation.add_comm,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────┘└─
205 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
206 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
207 end,
st ────┘
208 mul_comm := λ x y,
id ┴ ┴
typ ┴ ┴
209 begin
st └─────
210 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
211 induction y,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
212 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
213 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
214 apply relation.mul_comm,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────┘└─
215 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
216 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
217 end,
st ────┘
218 add_assoc := λ x y z,
id ┴ ┴ ┴
typ ┴ ┴ ┴
219 begin
st └─────
220 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
221 induction y,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
222 induction z,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
223 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
224 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
225 apply relation.add_assoc,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────┘└─
226 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
227 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
228 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
229 end,
st ────┘
230 mul_assoc := λ x y z,
id ┴ ┴ ┴
typ ┴ ┴ ┴
231 begin
st └─────
232 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
233 induction y,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
234 induction z,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
235 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
236 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
237 apply relation.mul_assoc,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────┘
238 refl,
239 refl,
240 refl,
st └─
241 end,
st ────┘
242 left_distrib := λ x y z,
id ┴ ┴ ┴
typ ┴ ┴ ┴
243 begin
244 induction x,
245 induction y,
246 induction z,
247 dsimp,
248 apply quot.sound,
249 apply relation.left_distrib,
250 refl,
251 refl,
252 refl,
st └─
253 end,
st ────┘
254 right_distrib := λ x y z,
id ┴ ┴ ┴
typ ┴ ┴ ┴
255 begin
256 induction x,
257 induction y,
258 induction z,
259 dsimp,
260 apply quot.sound,
261 apply relation.right_distrib,
262 refl,
263 refl,
264 refl,
st └─
265 end, }
st ────┘
266
267 @[simp] lemma quot_zero : quot.mk setoid.r zero = (0 : colimit_type F) := rfl
id └─────┘ └──────┘ └──┘ ┴ └──────────┘ ┴ └─┘
src └──────┘ └──┘ ┴ └──────────┘ └─┘
typ └─────┘ └──────┘ └──┘ ┴ └──────────┘ ┴ └─┘
doc └──┘
268 @[simp] lemma quot_one : quot.mk setoid.r one = (1 : colimit_type F) := rfl
id └─────┘ └──────┘ └─┘ ┴ └──────────┘ ┴ └─┘
src └──────┘ └─┘ ┴ └──────────┘ └─┘
typ └─────┘ └──────┘ └─┘ ┴ └──────────┘ ┴ └─┘
doc └──┘
269 @[simp] lemma quot_neg (x) : quot.mk setoid.r (neg x) = (-(quot.mk setoid.r x) : colimit_type F) := rfl
id └─────┘ └──────┘ └─┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴ └──────────┘ ┴ └─┘
src └──────┘ └─┘ ┴ ┴ └──────┘ └──────────┘ └─┘
typ └─────┘ └──────┘ └─┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴ └──────────┘ ┴ └─┘
doc └──┘
270 @[simp] lemma quot_add (x y) : quot.mk setoid.r (add x y) = ((quot.mk setoid.r x) + (quot.mk setoid.r y) : colimit_type F) := rfl
id └─────┘ └──────┘ └─┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴ ┴ └─────┘ └──────┘ ┴ └──────────┘ ┴ └─┘
src └──────┘ └─┘ ┴ └──────┘ ┴ └──────┘ └──────────┘ └─┘
typ └─────┘ └──────┘ └─┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴ ┴ └─────┘ └──────┘ ┴ └──────────┘ ┴ └─┘
doc └──┘
271 @[simp] lemma quot_mul (x y) : quot.mk setoid.r (mul x y) = ((quot.mk setoid.r x) * (quot.mk setoid.r y) : colimit_type F) := rfl
id └─────┘ └──────┘ └─┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴ ┴ └─────┘ └──────┘ ┴ └──────────┘ ┴ └─┘
src └──────┘ └─┘ ┴ └──────┘ ┴ └──────┘ └──────────┘ └─┘
typ └─────┘ └──────┘ └─┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴ ┴ └─────┘ └──────┘ ┴ └──────────┘ ┴ └─┘
doc └──┘
272
273 def colimit : CommRing := CommRing.of (colimit_type F)
id └──────┘ └─────────┘ └──────────┘ ┴
src └──────┘ └─────────┘ └──────────┘
typ └──────┘ └─────────┘ └──────────┘ ┴
doc └──────┘ └─────────┘
274
275 def cocone_fun (j : J) (x : F.obj j) : colimit_type F :=
id ┴ ┴└──┘ ┴ └──────────┘ ┴
src └──┘ └──────────┘
typ ┴ ┴└──┘ ┴ └──────────┘ ┴
276 quot.mk _ (of j x)
id └─────┘ └┘ ┴ ┴
src └┘
typ └─────┘ └┘ ┴ ┴
277
278 def cocone_morphism (j : J) : F.obj j ⟶ colimit F :=
id ┴ ┴└──┘ ┴ ┴ └─────┘ ┴
src └──┘ ┴ └─────┘
typ ┴ ┴└──┘ ┴ ┴ └─────┘ ┴
279 { to_fun := cocone_fun F j,
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
280 map_one' := by apply quot.sound; apply relation.one,
id └────────┘ └──────────┘
src └────┘└────────┘ └────┘└──────────┘
typ └────┘└────────┘ └────┘└──────────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st └───────────────────────────────────┘
281 map_mul' := by intros; apply quot.sound; apply relation.mul,
id └────────┘ └──────────┘
src └────┘ └────┘└────────┘ └────┘└──────────┘
typ └────┘ └────┘└────────┘ └────┘└──────────┘
doc └────┘ └────┘ └────┘
txt └────┘ └────┘ └────┘
par └────┘ └────┘ └────┘
pid ┴ ┴
st └───────────────────────────────────────────┘
282 map_zero' := by apply quot.sound; apply relation.zero,
id └────────┘ └───────────┘
src └────┘└────────┘ └────┘└───────────┘
typ └────┘└────────┘ └────┘└───────────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st └────────────────────────────────────┘
283 map_add' := by intros; apply quot.sound; apply relation.add }
id └────────┘ └──────────┘
src └────┘ └────┘└────────┘ └────┘└──────────┘┴
typ └────┘ └────┘└────────┘ └────┘└──────────┘┴
doc └────┘ └────┘ └────┘ ┴
txt └────┘ └────┘ └────┘ ┴
par └────┘ └────┘ └────┘ ┴
pid ┴ ┴ ┴
st └────────────────────────────────────────────┘
284
285 @[simp] lemma cocone_naturality {j j' : J} (f : j ⟶ j') :
id ┴ ┴ ┴ └┘
src ┴
typ ┴ ┴ ┴ └┘
doc └──┘
286 F.map f ≫ (cocone_morphism F j') = cocone_morphism F j :=
id ┴└──┘ ┴ ┴ └─────────────┘ ┴ └┘ ┴ └─────────────┘ ┴ ┴
src └──┘ ┴ └─────────────┘ ┴ └─────────────┘
typ ┴└──┘ ┴ ┴ └─────────────┘ ┴ └┘ ┴ └─────────────┘ ┴ ┴
287 begin
st └─────
288 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
289 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────┘└─
290 apply relation.map,
id └──────────┘
src └────┘└──────────┘
typ └────┘└──────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
291 end
st ──┘
292
293 @[simp] lemma cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j):
id ┴ ┴ ┴ └┘ ┴└──┘ ┴
src ┴ └──┘
typ ┴ ┴ ┴ └┘ ┴└──┘ ┴
doc └──┘
294 (cocone_morphism F j') (F.map f x) = (cocone_morphism F j) x :=
id └─────────────┘ ┴ └┘ ┴└──┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘ └──┘ ┴ └─────────────┘
typ └─────────────┘ ┴ └┘ ┴└──┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
295 by { rw ←cocone_naturality F f, refl }
id └───────────────┘ ┴ ┴
src └──┘└───────────────┘┴ ┴ ┴
typ └──┘└───────────────┘┴┴┴┴ ┴
doc └──┘ ┴ ┴ ┴
txt └──┘ ┴ ┴ ┴
par └──┘ ┴ ┴ ┴
pid └┘ ┴ ┴
st ┴ └───────────────────────┘ └┘ └┘
296
297 def colimit_cocone : cocone F :=
298 { X := colimit F,
299 ι :=
300 { app := cocone_morphism F } }.
id ┴
src ┴
typ ┴
doc ┴
301
302 @[simp] def desc_fun_lift (s : cocone F) : prequotient F → s.X
doc └──┘
303 | (of j x) := (s.ι.app j) x
id ┴
typ ┴
304 | zero := 0
305 | one := 1
306 | (neg x) := -(desc_fun_lift x)
id ┴
typ ┴
307 | (add x y) := desc_fun_lift x + desc_fun_lift y
id ┴ ┴
typ ┴ ┴
308 | (mul x y) := desc_fun_lift x * desc_fun_lift y
id ┴ ┴
typ ┴ ┴
309
310 def desc_fun (s : cocone F) : colimit_type F → s.X :=
311 begin
312 fapply quot.lift,
313 { exact desc_fun_lift F s },
st └┘
314 { intros x y r,
315 induction r; try { dsimp },
id └─┘
src └─┘
typ └─┘
doc └─┘
316 -- refl
317 { refl },
st └┘
318 -- symm
319 { exact r_ih.symm },
st └┘
320 -- trans
321 { exact eq.trans r_ih_h r_ih_k },
st └┘
322 -- map
323 { rw cocone.naturality_concrete, },
st └┘
324 -- zero
325 { erw is_ring_hom.map_zero ⇑((s.ι).app r), refl },
id ┴
typ ┴
st └┘
326 -- one
327 { erw is_ring_hom.map_one ⇑((s.ι).app r), refl },
id ┴
typ ┴
st └┘
328 -- neg
329 { rw is_ring_hom.map_neg ⇑((s.ι).app r_j) },
id └─┘
typ └─┘
st └┘
330 -- add
331 { rw is_ring_hom.map_add ⇑((s.ι).app r_j) },
id └─┘
typ └─┘
st └┘
332 -- mul
333 { rw is_ring_hom.map_mul ⇑((s.ι).app r_j) },
id └─┘
typ └─┘
st └┘
334 -- neg_1
335 { rw r_ih, },
st └┘
336 -- add_1
337 { rw r_ih, },
st └┘
338 -- add_2
339 { rw r_ih, },
st └┘
340 -- mul_1
341 { rw r_ih, },
st └┘
342 -- mul_2
343 { rw r_ih, },
st └┘
344 -- zero_add
345 { rw zero_add, },
st └┘
346 -- add_zero
347 { rw add_zero, },
st └┘
348 -- one_mul
349 { rw one_mul, },
st └┘
350 -- mul_one
351 { rw mul_one, },
st └┘
352 -- add_left_neg
353 { rw add_left_neg, },
st └┘
354 -- add_comm
355 { rw add_comm, },
st └┘
356 -- mul_comm
357 { rw mul_comm, },
st └┘
358 -- add_assoc
359 { rw add_assoc, },
st └┘
360 -- mul_assoc
361 { rw mul_assoc, },
st └┘
362 -- left_distrib
363 { rw left_distrib, },
st └┘
364 -- right_distrib
365 { rw right_distrib, },
st └┘
366 }
st └─
367 end
st ──┘
368
369 @[simp] def desc_morphism (s : cocone F) : colimit F ⟶ s.X :=
doc └──┘
370 { to_fun := desc_fun F s,
371 map_one' := rfl,
372 map_zero' := rfl,
373 map_add' := λ x y, by { induction x; induction y; refl },
id └──┘
src └──┘
typ └──┘
doc └──┘
st └┘
374 map_mul' := λ x y, by { induction x; induction y; refl }, }
id └──┘
src └──┘
typ └──┘
doc └──┘
st └┘
375
376 def colimit_is_colimit : is_colimit (colimit_cocone F) :=
377 { desc := λ s, desc_morphism F s,
id ┴
src ┴
typ ┴
doc ┴
378 uniq' := λ s m w,
379 begin
380 ext,
381 induction x,
382 induction x,
id ┴
typ ┴
383 { have w' := congr_fun (congr_arg (λ f : F.obj x_j ⟶ s.X, (f : F.obj x_j → s.X)) (w x_j)) x_x,
id └─┘
typ └─┘
384 erw w',
385 refl, },
st └┘
386 { simp only [desc_morphism, quot_zero],
387 erw is_ring_hom.map_zero ⇑m,
388 refl, },
st └┘
389 { simp only [desc_morphism, quot_one],
390 erw is_ring_hom.map_one ⇑m,
391 refl, },
st └┘
392 { simp only [desc_morphism, quot_neg],
393 erw is_ring_hom.map_neg ⇑m,
394 rw [x_ih],
395 refl, },
st └┘
396 { simp only [desc_morphism, quot_add],
397 erw is_ring_hom.map_add ⇑m,
398 rw [x_ih_a, x_ih_a_1],
399 refl, },
st └┘
400 { simp only [desc_morphism, quot_mul],
401 erw is_ring_hom.map_mul ⇑m,
402 rw [x_ih_a, x_ih_a_1],
403 refl, },
st └┘
404 refl
405 end }.
st └─┘
406
407 instance has_colimits_CommRing : has_colimits.{v} CommRing.{v} :=
id └──┘ └┘
src └──┘ └┘
typ └──┘ └┘
doc └──┘ └┘
408 { has_colimits_of_shape := λ J 𝒥,
id ┴ ┴
typ ┴ ┴
409 { has_colimit := λ F, by exactI
410 { cocone := colimit_cocone F,
411 is_colimit := colimit_is_colimit F } } }
412
413 end CommRing.colimits